r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a).
(w:|r|. SqStable(a(w)))  (u, v:|r|. (u = v  |r / d|)  (a(u +r (-r(v))))) 

latex

Up	rings 1
Definitions of Statement	|r|, Rng, CRng, Ideal(r){i}, r / d
Definitions	, t  T, P  Q, x:A. B(x), t.1, r / d, |r|, P & Q, P  Q, x f y, P  Q, Rng, Ideal(r){i}, CRng, detach_fun(T;A), S  T
Lemmas	crng wf, ideal wf, detach fun wf, sq stable wf, rng car wf, quot ring car elim, rng minus wf, rng plus wf, assert wf, quot ring car qinc, quot ring car wf, iff functionality wrt iff, det ideal ap elim